Motivation for this change

this PR adds a lemma to mathcomp_extra.v that generalizes a lemma of finmap,
the same lemma has also been PRed to finmap but we need a local copy in the meantime,
this is used to prove properties of independence of random variables and it is
better to have it in master asap to avoid recompilation from classical when switching branches

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels